/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package compiledriver;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.ListIterator;

/**
 *
 * @author wynd
 */
public class Environment {
    private ListIterator<String> myIterator;
    private HashMap<String, Definition> defHash = new HashMap<String, Definition>();
    private HashMap<String, Operation> opHash = new HashMap<String, Operation>();
    private ArrayList<Procedure> procList = new ArrayList<Procedure>();
    private String proofString = "";
    
    public Environment(ListIterator<String> newIterator)
    {
        myIterator = newIterator;
        createEnvironment();
    }

    private void createEnvironment(){
        while(myIterator.hasNext()){
            String itString = myIterator.next();
            if(itString.equals("Definition")){
                Definition def = new Definition(myIterator);
                defHash.put(def.getId(), def);
            }
            else if(itString.equals("Operation")){
                Operation op = new Operation(myIterator, defHash);
                opHash.put(op.getId(), op);
            }
            else if(itString.equals("Procedure")){
                Procedure proc = new Procedure(myIterator, defHash, opHash);
                procList.add(proc);
            }
        }
    }
    
    /**
     * Pulls the corresponding <code>Operation</code>s from the passed in callList
     * @param callList
     * @return 
     */
    public ArrayList<Operation> getOperations(ArrayList<Call> callList){
        ArrayList<Operation> retList = new ArrayList();
        for(Call c: callList){
            Operation t = opHash.get(c.getId());
            if(t == null){
                throw new IllegalStateException("Did not find operation for call"
                        + " " + c.getId());
            }
            retList.add(t);
        }
        return retList;
    }
    
    /**
     * Creates a <code>Map</code> by using unique values of the first 
     * <code>ArrayList</code> as keys and the unique values of the second as the values.
     * @param key An <code>ArrayList</code> of <code>String</code>s to use as keys
     * @param value An <code>ArrayList</code> of <code>String</code>s to use as values
     * @return A <code>Map</code> containing the unique values of the 
     * passed in <code>ArrayList</code>s
     */
    public HashMap<String, String> setExpressionMap(ArrayList<String> key, ArrayList<String> value){
        HashMap retMap = new HashMap();
        int count = 0;
        for(int i = 0; i < key.size(); i++){
            if(!retMap.containsKey(key.get(i))) {
                retMap.put(key.get(i), value.get(count));
                count++;
            }
        }
        return retMap;
    }
    
    public String proofTable(){
        Expression changed;
        ArrayList<Operation> operationList;
        HashMap<String, String> expressionMap;
        for(Procedure curr : procList){
            ArrayList<Call> currCall = curr.getCallList();
            operationList = getOperations(currCall);
            
            proofString += "Proof Table for [" + curr.getId() + "]\n\n";
            proofString += "State 0\n========\nAssuming:\n";
            
            expressionMap = setExpressionMap(curr.getRequires().getArguments(),
                    curr.getRequires().getArguments());
            changed = curr.getRequires().substitute(expressionMap, 0);
            proofString += changed.toString() + "\n";
            
            for(int i = 0; i < operationList.size(); i++){
                expressionMap = setExpressionMap(
                        operationList.get(i).getRequires().getArguments(), 
                        currCall.get(i).allArguments());
                changed = operationList.get(i).getRequires().substitute(expressionMap, i);
                proofString += "\nConfirm:\n" + changed.toString() + "\n\n";
                
                expressionMap = setExpressionMap(
                        operationList.get(i).getEnsures().getArguments(), 
                        currCall.get(i).allArguments());
                changed = operationList.get(i).getEnsures().substitute(expressionMap, i+1);
                proofString += "State " + (i+1) + "\n========\nAssuming:\n";
                proofString += changed.toString() + "\n";
            }
            expressionMap = setExpressionMap(
                    curr.getEnsures().getArguments(),curr.getEnsures().getArguments());
            changed = curr.getEnsures().substitute(expressionMap, operationList.size());
            proofString += "\nConfirm:\n" + changed.toString();
        }
        return proofString;
    }

    public ArrayList<Procedure> getProcList(){
        return procList;
    }
}
